the_es:ES, e':E, l:IdLnk, n:(||sends(l;e')||+1).
snds(l, before(e',n)) = nil  (Msg on l) List
 (e:E, m:||sends(l;e)||.
 ((e <loc e')  e = e' & m<n
 (& snds(l, before(e',n)) = (snds(l, before(e,m)) @ [sends(l;e)[m]])  (Msg on l) List
 (& (e'':E, k:.
 (& ((e <loc e'')  e = e'' & m<k & (e'' <loc e')  e'' = e' & k<n  ||sends(l;e'')||k)) 

latex

Definitions

{T}, P  Q, x:A. B(x), SQType(T), t  T, Prop, ||as||, False, A, P & Q, AB, i  j < k, {i..j}, P  Q, Dec(P), ES, E, IdLnk, sends(l;e), (Msg on l), snds(l, before(e,n)), (e <loc e'), , x:A. B(x), snds(l;before(e)), Top, S  T, l[i], as @ bs, before(e), map(f;as), True, last(L), T, P  Q, P  Q, null(as), b, ij, hd(l), tl(l), firstn(n;as), nth_tl(n;as), l1  l2, {i...j}, (x  l), A & B, t  ...$L, concat(ll), haslink(l;m), Msg, 1of(t), Trans x,y:T. E(x;y)

Lemmas

es-locl-antireflexive, es-axioms, firstn decomp2, add functionality wrt eq, concat-cons, concat-nil, map append sq, concat append, cons one one, es-Msg wf, member wf, es-before-decomp, length zero, firstn last, firstn-before, concat wf, append assoc sq, length nil, length cons, select member, member-es-before, select firstn, length firstn, map is append, map is cons, tl wf, hd wf, ge wf, nth tl wf, firstn wf, firstn firstn, non neg length, not functionality wrt iff, assert of null, assert wf, null wf, iseg length, squash wf, true wf, length append, map length, last wf, last-concat, map wf, es-before wf, append wf, select wf, nat wf, es-locl wf, le wf, first0, append nil sq, top wf, es-snds wf, not wf, es-snds-index wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, IdLnk wf, es-E wf, event system wf, decidable int equal